fail{-}dcdr\{i:l\}(${\it es}$;${\it Fail}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$TERMOF\{decidable\_\_exists{-}fail:ObjectId, 1:l, i:l\}(${\it es}$,${\it Fail}$)